Nuprl Lemma : rng_car_qinc
13,42
postcript
pdf
r
:CRng,
a
:Ideal(
r
){i},
d
:detach_fun(|
r
|;
a
). |
r
|
|
r
/
d
|
latex
Up
rings
1
Definitions of Statement
|
r
|
,
r
/
d
Definitions
t
.1
,
r
/
d
,
|
r
|
Lemmas
quot
ring
car
qinc
origin
r:CRng, a:Ideal(r){i}, d:detach_fun(|r|;a). |r| 
|r / d| r:CRng, a:Ideal(r){i}, d:detach_fun(|r|;a). |r| |r / d|